T:Type, dT:EqDecider(T), L:(T List), x, y:T.
(x  L)  (y  L)  (index(L;x) < index(L;y))  x before y  L 

latex

Definitions	x:A. B(x), P  Q, t  T, , T, True, P  Q, P  Q, P & Q, {i..j}
Lemmas	l index wf, int seg wf, length wf1, l member wf, deq wf, l before select, l before wf, squash wf, true wf, select l index